Nuprl Definition : scheme-compatible 11,40

scheme-compatible(A;B)
== let na,La,Ra = A in 
== let nb,Lb,Rb = B in 
== nmr_a:Namer(na;La), nmr_b:Namer(nb;Lb).
== namer-disjoint(na;nb;nmr_a;nmr_b Ra(nmr_a) || Rb(nmr_b
latex



clarification:

scheme-compatible{i:l}
scheme-compatible(AB)
== let na,La,Ra = A in 
== let nb,Lb,Rb = B in 
== nmr_a:Namer(na;La), nmr_b:Namer(nb;Lb).
== namer-disjoint(na;nb;nmr_a;nmr_b R-compat{i:l}((Ra(nmr_a)); (Rb(nmr_b))) 
latex


Definitionslet x,y,z = a in t(x;y;z), x:AB(x), Namer(n;Id_list), P  Q, A || B, f(a)
FDL editor aliasesscheme-compatible

origin